home *** CD-ROM | disk | FTP | other *** search
/ Columbia Kermit / kermit.zip / newsgroups / misc.19950528-19950726 / 000405_news@columbia.edu_Fri Jul 21 20:10:18 1995.msg < prev    next >
Internet Message Format  |  2020-01-01  |  3KB
  1. Received: from apakabar.cc.columbia.edu by watsun.cc.columbia.edu with SMTP id AA18084
  2.   (5.65c+CU/IDA-1.4.4/HLK for <kermit.misc@watsun.cc.columbia.edu>); Fri, 21 Jul 1995 16:59:43 -0400
  3. Received: by apakabar.cc.columbia.edu id AA19054
  4.   (5.65c+CU/IDA-1.4.4/HLK for kermit.misc@watsun); Fri, 21 Jul 1995 16:59:41 -0400
  5. Path: news.columbia.edu!panix!news.mathworks.com!newshost.marcam.com!zip.eecs.umich.edu!news-server.eecs.umich.edu!huggins
  6. From: huggins@tarski.eecs.umich.edu (James K. Huggins)
  7. Newsgroups: comp.protocols.kermit.misc
  8. Subject: Kermit Proof of Correctness Available
  9. Followup-To: comp.protocols.kermit.misc
  10. Date: 21 Jul 1995 20:10:18 GMT
  11. Organization: University of Michigan EECS Dept., Ann Arbor, MI
  12. Lines: 38
  13. Distribution: world
  14. Message-Id: <HUGGINS.95Jul21161018@tarski.eecs.umich.edu>
  15. Nntp-Posting-Host: tarski.eecs.umich.edu
  16. Apparently-To: kermit.misc@watsun.cc.columbia.edu
  17.  
  18. In his preface to Frank da Cruz's book Kermit: A File Transfer
  19. Protocol, Don Knuth wrote:
  20.  
  21.      I hope that many readers of this book will be challenged to find
  22.      high-level concepts and invariant relations by which various
  23.      versions of the Kermit protocol can be proved correct in a
  24.      mathematical sense.
  25.  
  26. I'm pleased to announce that such a proof has recently been completed.
  27. The proof gives a complete specification of the core Kermit file
  28. transfer protocol, and shows that it is both safe (if you get a file,
  29. you can be sure it's the one that was sent) and live (if you send
  30. a file, and the network isn't too bad, it gets to the other end).
  31.  
  32. The proof (written by myself) appears as part of a new book,
  33. "Specification and Validation Methods", edited by Egon Boerger
  34. and available through Oxford University Press (ISBN 0-19-853854-5,
  35. official publishing date 3 August 1995).  
  36.  
  37. Thanks to the good folks at Oxford University Press, as well as Frank
  38. da Cruz at Columbia, the Kermit proof has been made available 
  39. as part of the Kermit repository at Columbia University.  Those of
  40. you with WWW access can find the cover page for the proof, including
  41. more detailed information on the book containing the proof, at
  42.  
  43.     http://www.columbia.edu/kermit/proof.html   
  44.  
  45. The proof itself (in PostScript) is available via anonymous FTP as
  46.  
  47.     ftp://kermit.columbia.edu/kermit/e/proof.ps      
  48.  
  49. As the author of the proof, I'd be happy to hear any comments or
  50. questions you might have about the proof.  The proof uses a relatively
  51. new specification methodology known as "evolving algebras"; an
  52. introduction to the method is contained in the proof.  I'd be happy
  53. to discuss the technique with anyone who might be interested.
  54.  
  55. Jim Huggins (huggins@umich.edu)